/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Rewrite database
 */

#include "cvc5_private.h"

#ifndef CVC5__REWRITER__REWRITE_DB__H
#define CVC5__REWRITER__REWRITE_DB__H

#include <map>
#include <vector>

#include "expr/nary_match_trie.h"
#include "expr/nary_term_util.h"
#include "expr/node.h"
#include "expr/term_canonize.h"
#include "rewriter/rewrites.h"

namespace cvc5::internal {
namespace rewriter {

/**
 * A database of conditional rewrite rules. The rules of this class are
 * automatically populated based on the compilation of the rewrite rule files.
 */
class RewriteDb
{
 public:
  /**
   * Constructor. The body of this method is auto-generated by the rules
   * defined in the rewrite_rules files.
   */
  RewriteDb();
  ~RewriteDb() {}
  /** Add rule id to this database
   *
   * @param id The identifier of the rule
   * @param fvs The free variables of the rule
   * @param a The left hand side of the rule
   * @param b The right hand side of the rule
   * @param cond The condition, or null if this is not a conditional rule
   * @param context The term context, if one exists
   * @param isFlatForm Whether the rule is in flat form
   */
  void addRule(DslPfRule id,
               const std::vector<Node> fvs,
               Node a,
               Node b,
               Node cond,
               Node context,
               bool isFlatForm = false);
};

}  // namespace rewriter
}  // namespace cvc5::internal

#endif /* CVC4__THEORY__REWRITE_DB__H */
